i,j:. ((i = j) = ff  )  i  j 

latex

ProofTree

Definitions	, t  T, P  Q, x:A. B(x), a  b  T , P  Q, P  Q, P  Q, P  Q, Dec(P), False, A
Lemmas	bfalse wf, eq int wf, bool wf, decidable int equal, eq int eq true, btrue neq bfalse